Sistema formal

Un sistema formal o axiomàtic és un artifici matemàtic compost de símbols que s'uneixen entre si formant cadenes que, al seu torn, poden ser manipulades segons regles per produir altres cadenes. D'aquesta manera, el sistema formal és capaç de representar cert aspecte de la realitat. El terme «formalisme» s'utilitza, de vegades, com a sinònim de sistema formal, per a un determinat propòsit. Un sistema formal matemàtic consisteix en el següent:

1. Un conjunt finit de símbols que poden ser usats per a la construcció de fórmules.
2. Una gramàtica, és a dir, un mecanisme per a la construcció de fórmules ben formades (WFF). També s'ha de proporcionar un algorisme de decisió per conèixer si una determinada fórmula és ben formada o no.
3. Un conjunt d'axiomes que han de ser fórmules WFF.
4. Un conjunt de regles d'inferència.
5. Un conjunt de teoremes. Aquest conjunt inclou tots els axiomes, més totes les WFF que poden ser derivades dels axiomes o d'altres teoremes per mitjà de les regles d'inferència. La gramàtica no necessàriament garanteix la decidibilitat de si una fórmula és teorema o no.

En les ciències formals de la lògica i les matemàtiques, així com en altres disciplines relacionades, com són la informàtica, la teoria de la informació, i l'estadística, un sistema formal és una gramàtica formal usada per a la modelització de diferents propòsits. S'anomena formalització l'acte de crear un sistema formal, i es tracta d'una acció amb la qual pretenem capturar i abstreure l'essència de determinades característiques del món real, en un model conceptual expressat en un determinat llenguatge formal.

En matemàtiques, les proves formals són el resultat de sistemes formals, consistents en axiomes i regles de deducció. Els teoremes poden ser obtinguts per mitjà de proves formals. Aquest punt de vista de les matemàtiques ha estat anomenat formalista, encara que moltes vegades aquest terme comporta una accepció pejorativa. En aquest sentit, David Hilbert va crear la disciplina anomenada metamatemàtica, dedicada a l'estudi dels sistemes formals, entenent que el llenguatge utilitzat per a això, anomenat metallenguatge, era diferent del llenguatge del sistema formal que es pretenia estudiar. Amb una altra denominació, el metallenguatge o llenguatge obtingut mitjançant la gramàtica formal es diu també, a vegades, llenguatge objecte.

Un sistema així és la reducció d'un llenguatge formalitzat a mers símbols, llenguatge formalitzat i simbolitzat sense cap contingut material; un llenguatge reduït a mera forma que s'expressa mitjançant fórmules que reflecteixen les relacions sintàctiques entre els símbols i les regles de formació i transformació que permeten construir les fórmules del sistema i passar d'una fórmula a una altra.

L'objectiu d'un sistema formal és assenyalar com a vàlides determinades cadenes. Aquestes cadenes vàlides es denominen teoremes. Per a obtenir els teoremes, es fan servir les regles de producció que converteixen una cadena en una altra. Hi ha certs teoremes inicials que no s'obtenen de cap regla, aquests són els axiomes que se suposen vàlids per definició i es converteixen en el germen de producció de teoremes.